﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Xml;
using System.Diagnostics.Contracts;

namespace HeapModel.ProgInfo
{
	/// <summary>
	/// A base class for representing simple program indentifiers. 
	/// This includes Variables, Member Fields, Class Fields, and Types.
	/// 
	/// We will use an intern table later to ensure that each name is unique (for space efficiency and to allow quick comparision).
	/// </summary>
	public abstract class Identifier
	{
		private readonly string m_name; //The name as a string

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{ Contract.Invariant(!String.IsNullOrEmpty(this.m_name)); }

		protected Identifier(String name)
		{
			Contract.Requires(!String.IsNullOrEmpty(name));

			this.m_name = name;
		}

		public override String ToString()
		{ return this.NameValue; }

		public String NameValue
		{
			get
			{
				Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<String>()));

				return this.m_name;
			}
		}
	}

	/// <summary>
	/// A subclass to represent program identifiers that refer to types. Includes basic information on subtypes and visible pointer 
	/// fields (includes all fields including private). Also we encode some information on how to treat the types from the perspective 
	/// of the visulization.
	/// Note: Pointers are assumed to have an offset of the empty access path, and the type of this offset is the type of the dereferenced pointer. 
	/// Note: Subtyping does not exist (e.g. no way to define a type tree) but the types of the offsets are given as SETS so you can just load entire 
	/// subtype trees into these sets for the same effect wrt. visualization.
	/// </summary>
	public sealed class TypeIdentifier : Identifier
	{
		/// <summary>
		/// We want to treat types differently during the abstraction and processing. 
		/// Ignore is a type that refers to an "uninteresting" type, either a system type or some type outside of the namespace of interest.
		/// </summary>
		public enum TypeCategory 
		{
 			Value = 0x0,
			Object = 0x1,
			Array = 0x2,      
			List = 0x3,
			Set = 0x4,
			KeyValPair = 0x5,
			Dictionary = 0x6, 
			Null = 0x7
		};

		/// <summary>
		/// The size of the object headers for any class.
		/// </summary>
		public const int OBJECT_HEADER_SIZE = 8;

		/// <summary>
		/// The number of bytes needed for an array in addition the object header (i.e. the length field).
		/// </summary>
		public const int ARRAY_SIZE_OVERHEAD = 4;

		/// <summary>
		/// The number of bytes needed for a list in addition the object header (i.e. the pointer + count).
		/// </summary>
		public const int LIST_SIZE_OVERHEAD = 8;

		/// <summary>
		/// The minimum capcity that a list maintains (e.g. the empty list does not have length 0).
		/// </summary>
		public const int LIST_MIN_CAPCITY = 4;

		/// <summary>
		/// The minimum number of bytes in addition the object header (i.e. the count field, the pointer, etc.).
		/// </summary>
		public const int HASHSET_SIZE_OVERHEAD = 12;

		/// <summary>
		/// The minimum capcity that a set maintains (e.g. the empty set does not have length 0).
		/// </summary>
		public const int HASHSET_MIN_CAPCITY = 8;

		/// <summary>
		/// The hashset uses a hashtable, and in order to prevent collisions must have space for approx 2x as many entries as are present.
		/// </summary>
		public const int HASHSET_SIZE_CAPACITY_FACTOR = 2;

		/// <summary>
		/// The minimum number of bytes in addition the object header (i.e. the count field, the pointer, etc.).
		/// </summary>
		public const int DICTIONARY_SIZE_OVERHEAD = 12;

		/// <summary>
		/// The minimum capcity that a dictionary maintains (e.g. the empty dictionary does not have length 0).
		/// </summary>
		public const int DICTIONARY_MIN_CAPCITY = 8;

		/// <summary>
		/// The dictionary uses a hashtable, and in order to prevent collisions must have space for approx 2x as many entries as are present.
		/// </summary>
		public const int DICTIONARY_SIZE_CAPACITY_FACTOR = 2;

		private TypeCategory m_typecat;
		private readonly List<OffsetIdentifier> m_alloffsetidentifiers;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.m_alloffsetidentifiers != null);
		}

		/// <summary>
		/// Create a type identifier without any subtype of field information, this should be filled in later.
		/// </summary>
		public TypeIdentifier(String name, TypeCategory tc)
			: base(name)
		{
			Contract.Requires(!String.IsNullOrEmpty(name));

			this.m_typecat = tc;
			this.m_alloffsetidentifiers = new List<OffsetIdentifier>();
		}

		/// <summary>
		/// Write out the type name for serialization to an xml file.
		/// </summary>
		public void SerializeTypeName(XmlWriter xmlw)
		{
			Contract.Requires(xmlw != null);

			xmlw.WriteStartElement("TypeDef");

			xmlw.WriteAttributeString("Name", this.NameValue);
			xmlw.WriteAttributeString("Category", ((int)this.m_typecat).ToString());

			xmlw.WriteStartElement("ContainedOffsets");
			for(int i = 0; i < this.m_alloffsetidentifiers.Count; ++i)
				xmlw.WriteElementString("OffsetName", this.m_alloffsetidentifiers[i].NameValue);
			xmlw.WriteEndElement();

			xmlw.WriteEndElement();
		}

		/// <summary>
		/// Return partially instantiated type, list of subtype names, and list of allvisptrfield names.
		/// The dual for the <c>SerializeTypeName</c> method.
		/// </summary>
		public static TypeParseInfo ReadTypeNameDef(XmlReader rr, Dictionary<String, TypeIdentifier> tymap)
		{
			Contract.Requires(rr != null);
			Contract.Requires(tymap != null);
			Contract.Ensures(Contract.Result<TypeParseInfo>() != null);

			String name = rr.GetAttribute("Name");
			TypeCategory catval = (TypeCategory)Int32.Parse(rr.GetAttribute("Category"));

			TypeIdentifier retty;
			if(tymap.ContainsKey(name))
				retty = tymap[name];
			else
			{
				retty = new TypeIdentifier(name, catval);
				tymap.Add(name, retty);
			}

			rr.ReadStartElement("TypeDef");
			List<String> vfl = new List<String>();

			if(rr.IsEmptyElement)
				rr.ReadStartElement("ContainedOffsets");
			else
			{
				rr.ReadStartElement("ContainedOffsets");
				while(rr.IsStartElement("OffsetName"))
				{
					rr.ReadStartElement("OffsetName");
					String fname = rr.ReadString();
					vfl.Add(fname);
					rr.ReadEndElement();
				}
				rr.ReadEndElement();
			}

			rr.ReadEndElement();

			return new TypeParseInfo(retty, vfl);
		}

		public TypeCategory TypeCategoryTag
		{
			get { return this.m_typecat; }
			set { this.m_typecat = value; }
		}

		public bool IsValueType
		{ get { return this.m_typecat == TypeCategory.Value; } }

		public bool IsObjectType
		{ get { return this.m_typecat == TypeCategory.Object; } }

		public bool IsArrayType
		{ get { return this.m_typecat == TypeCategory.Array; } }

		public bool IsListType
		{ get { return this.m_typecat == TypeCategory.List; } }

		public bool IsSetType
		{ get { return this.m_typecat == TypeCategory.Set; } }

		public bool IsKeyValType
		{ get { return this.m_typecat == TypeCategory.KeyValPair; } }

		public bool IsDictionaryType
		{ get { return this.m_typecat == TypeCategory.Dictionary; } }

		public bool IsCollectionType
		{ get { return (this.m_typecat == TypeCategory.Array) | (this.m_typecat == TypeCategory.List) | (this.m_typecat == TypeCategory.Set) | (this.m_typecat == TypeCategory.Dictionary); } }

		public bool IsSpecialNullType
		{ get { return this.m_typecat == TypeCategory.Null; } }

		public List<OffsetIdentifier> AllOffsetIdentifiers
		{ 
			get 
			{
				Contract.Ensures(Contract.Result<List<OffsetIdentifier>>() != null);

				return this.m_alloffsetidentifiers; 
			} 
		}
	}

	/// <summary>
	/// A subclass to represent member field identifiers.
	/// </summary>
	public sealed class OffsetIdentifier : Identifier
	{
		private readonly HashSet<TypeIdentifier> m_offsettypes; //type of the values that may be stored in this field.

		[ContractInvariantMethod]
		private void MemberFieldIdentifierInvariant()
		{
			Contract.Invariant(this.m_offsettypes != null);
		}

		public OffsetIdentifier(String name, HashSet<TypeIdentifier> offsettypes)
			: base(name)
		{
			Contract.Requires(!String.IsNullOrEmpty(name));
			Contract.Requires(offsettypes != null);

			this.m_offsettypes = offsettypes;
		}

		/// <summary>
		/// Write out the offsetidentifier for serialization to an xml file.
		/// </summary>
		public void SerializeOffsetIdentifier(XmlWriter xmlw)
		{
			Contract.Requires(xmlw != null);

			xmlw.WriteStartElement("OffsetIdentifier");
			xmlw.WriteAttributeString("Name", this.NameValue);
			
			xmlw.WriteStartElement("OffsetTypes");
			foreach(TypeIdentifier subtt in this.m_offsettypes)
				xmlw.WriteElementString("TypeID", subtt.NameValue);
			xmlw.WriteEndElement();

			xmlw.WriteEndElement();
		}

		/// <summary>
		/// Return instantiated offsetidentifier.
		/// </summary>
		public static OffsetIdentifier ReadOffsetIdentifier(XmlReader rr, Dictionary<String, TypeIdentifier> tydict)
		{
			Contract.Requires(rr != null);
			Contract.Requires(tydict != null);
			Contract.Ensures(Contract.Result<OffsetIdentifier>() != null);

			String namestr = rr.GetAttribute("Name");

			rr.ReadStartElement("OffsetIdentifier");
			HashSet<TypeIdentifier> offsettypes = new HashSet<TypeIdentifier>();

			if(rr.IsEmptyElement)
				rr.ReadStartElement("OffsetTypes");
			else
			{
				rr.ReadStartElement("OffsetTypes");
				while(rr.IsStartElement("TypeID"))
				{
					rr.ReadStartElement("TypeID");
					String typename = rr.ReadString();
					offsettypes.Add(tydict[typename]);
					rr.ReadEndElement();
				}
				rr.ReadEndElement();
			}
			rr.ReadEndElement();

			return new OffsetIdentifier(namestr, offsettypes);
		}

		public HashSet<TypeIdentifier> OffsetTypes 
		{ 
			get 
			{
				Contract.Ensures(Contract.Result<HashSet<TypeIdentifier>>() != null);

				return this.m_offsettypes; 
			} 
		}
	}

	/// <summary>
	/// A helper tuple for parsing and expanding serialized type information.
	/// </summary>
	public sealed class TypeParseInfo
	{
		public readonly TypeIdentifier Item1;
		public readonly List<String> Item2;

		public TypeParseInfo(TypeIdentifier identifier, List<String> offsets)
		{
			Contract.Requires(identifier != null);
			Contract.Requires(offsets != null);

			this.Item1 = identifier;
			this.Item2 = offsets;
		}
	}

	/// <summary>
	/// A named access path build up of a series of offsets (think getelemptr from LLVM).
	/// We build up an intern table of these as we need them.
	/// </summary>
	public sealed class AccessPath : IComparable<AccessPath>
	{
		private readonly OffsetIdentifier[] m_path;

		/// <summary>
		/// This access path as a string.
		/// </summary>
		private readonly String m_pathstring;

		/// <summary>
		/// A arbitrary but unique integer for this access path.
		/// </summary>
		private readonly int m_sorttoken;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.m_path != null);
			Contract.Invariant(this.m_path.Length != 0);
		}

		public AccessPath(OffsetIdentifier[] pth, int sorttoken)
		{
			Contract.Requires(pth != null);

			this.m_path = pth;

			if(this.m_path.Length == 0)
				this.m_pathstring = "";
			else
			{
				StringBuilder sb = new StringBuilder();
				for(int i = 0; i < this.m_path.Length; ++i)
				{
					if(i != 0)
						sb.Append("^");
					sb.Append(this.m_path[i].NameValue);
				}

				this.m_pathstring = sb.ToString();
			}

			this.m_sorttoken = sorttoken;
		}

		public override String ToString()
		{ return this.m_pathstring; }

		public String PathString
		{ get { return this.m_pathstring; } }

		public OffsetIdentifier[] PathValue
		{ get { return this.m_path; } }

		public int CompareTo(AccessPath other)
		{ return this.m_sorttoken - other.m_sorttoken; }

		public OffsetIdentifier PathLast
		{ 
			get 
			{ 
				Contract.Ensures(Contract.Result<OffsetIdentifier>() != null);
				
				return this.m_path[this.m_path.Length -1]; 
			} 
		}

		public void XMLify(XmlWriter xmlw)
		{
			Contract.Requires(xmlw != null);

			xmlw.WriteStartElement("AccessPath");
			xmlw.WriteAttributeString("Path", this.m_pathstring);
			xmlw.WriteEndElement();
		}

		public static AccessPath DeXMLify(XmlReader xmlr, Dictionary<String, AccessPath> refdict, Dictionary<String, OffsetIdentifier> offsetdict, ref int sorttokenctr)
		{
			Contract.Requires(xmlr != null);
			Contract.Requires(refdict != null);
			Contract.Requires(offsetdict != null);
			Contract.Ensures(Contract.Result<AccessPath>() != null);

			String path = xmlr.GetAttribute("Path");
			xmlr.ReadStartElement();

			if(refdict.ContainsKey(path))
				return refdict[path];
			else
			{
				List<OffsetIdentifier> accp = new List<OffsetIdentifier>();
				int poss = 0;
				int pose = path.IndexOf('^');
				while(pose != -1)
				{
					String nps = path.Substring(poss, pose - poss);
					OffsetIdentifier noff = offsetdict[nps];
					accp.Add(noff);

					poss = pose + 1;
					pose = path.IndexOf('^', poss);
				}

				String lp = path.Substring(poss);
				OffsetIdentifier loff = offsetdict[lp];
				accp.Add(loff);

				AccessPath resaccp = new AccessPath(accp.ToArray(), sorttokenctr++);
				refdict.Add(path, resaccp);
				return resaccp;
			}
		}
	}
}
